(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)


include "arithmetics/nat.ma".
include "basics/bool.ma".
include "basics/lists/list.ma".
include "basics/logic.ma".

                                                  (*        *
                                                   *  Types *
                                                   *        *)
                                                   
inductive integer : Type[0] ≝
  int : bool → nat → integer. 

inductive struct_one : Type[0] ≝
  atom : integer→ struct_one
| unit : struct_one.

inductive operator : Type[0] ≝
  par : operator
| copar : operator
| seq : operator.  

inductive struct : Type[0] ≝
   base : struct_one → struct
|  lista : operator → list struct → struct.



                                                  (*            *
                                                   *  Notations *
                                                   *            *)
                                                   
notation "+x" with precedence 80 for @{int true $x}.
notation "-x" with precedence 80 for @{int false $x}.
notation "∘" with precedence 80 for @{(base unit))}.
(*Qui sarebbe bello poter usare i caratteri*)
notation "x+" with precedence 100 for @{(base (atom +($x)))}.  
notation "x^" with precedence 100 for @{(base (atom -($x)))}.

notation "〚 list0 x sep ; 〛" (*qui ci vorrebbe , *)
  non associative with precedence 90
  for @{(*create_struct *)(lista par ${fold right @'nil rec acc @{'cons $x $acc}})}.


notation "❨ list0 x sep ; ❩"  (*qui ci vorrebbe , *)
  non associative with precedence 90
  for @{(*create_struct *)(lista copar ${fold right @'nil rec acc @{'cons $x $acc}})}.
  
notation "❮ list0 x sep ; ❯"
  non associative with precedence 90
  for @{(*create_struct*) (lista seq ${fold right @'nil rec acc @{'cons $x $acc}})}.
  
  
notation "x ≡ y" with precedence 45
  for @{struct_eq $x $y}.
  
notation "x ⥤ y" with precedence 45
  for @{struct_reduce $x $y}.

notation "𝐒" with precedence 45 for @{struct}.


  

                                                  (*            *
                                                   *  Functions *
                                                   *            *)

definition eqb_op ≝ λo1,o2.match o1 with[
  par ⇒ match o2 with [ par ⇒ true | _ ⇒ false]
| copar ⇒ match o2 with [copar ⇒ true | _ ⇒ false ]
| seq ⇒ match o2 with [seq ⇒ true | _ ⇒ false]].
  
definition is_not_unit ≝λs.match s with [base t ⇒ match t with [  unit ⇒ false | _ ⇒ true ] | _ ⇒ true ].
definition filter_unit_base ≝ filter struct is_not_unit.

(* Remove ALL units from struct s, if s is different from unit*)
let rec filter_unit s≝  match s with [
    lista op l ⇒ lista op (filter_unit_base (map ? ? filter_unit l))
  | base t ⇒ base t].
  
definition neq_op_s ≝λo.λs. match s with [ lista op l ⇒ op≠o | _ ⇒ True].

definition neg_op ≝ λo. match o with [
  par   ⇒ copar
| copar ⇒ par
| seq   ⇒ seq ].


let rec neg s ≝
  match s with [
      lista op l ⇒ lista (neg_op op) (map ? ? neg l) 
    | base t ⇒ match t with [
               atom i ⇒ match i with [ int b n ⇒ base (atom (int (¬b) n)) ]
             | unit  ⇒ base unit  
    ]
  ].
  
let rec size_struct b ≝
  match b with [
     base  t ⇒ 1
  |  lista op l ⇒  (\fold[plus,1]_{i∈l} (size_struct i))].
  
   
  
let rec singleton s ≝ match s with [
  lista o l ⇒ match l with [
      nil ⇒ lista o l (*base unit*)
    | cons h tl ⇒ match tl with [
        nil ⇒ singleton h
      | cons h2 tl2 ⇒ lista o (map ? ? singleton l)]]
| base t ⇒ base t].

(*Set the nth element of l to e, if nth doesn't exist does nothing*)
let rec setth (A:Type[0]) (l:list A) (e:A) (n:nat) on n ≝ match n with [
  O ⇒ match l with [
    nil ⇒ [e]
  | cons h tl ⇒ e::tl]
| S x ⇒ match l with [
    nil ⇒ l (*Non si può settare*)
  | cons h tl ⇒ h::(setth A tl e x)]].
  
(*Swaps elements in n1,n2 position if n1 or n2 doesn't exist does nothing*)

definition list_swap ≝λA:Type[0].λl:list A.λn1,n2:nat.λd:A. 
  match (leb n1 (|l|) ∧ leb n2 (|l|) ) with [
    true ⇒ (
  let e1 ≝ nth n1 ? l (d(*Non viene mai usato*)) in
  let e2 ≝ nth n2 ? l (d(*Non viene mai  usato*)) in
    setth ? (setth ? l e2 n1) e1 n2)
  | false ⇒ l].  
                                          
                                                  (*                *
                                                   *      Lemmi     *
                                                   *  Dimostrazioni *
                                                   *                *)
                                                   
                                                   
                                    
 (*Induction on struct*)
theorem elim_struct : ∀P : 𝐒 → Prop. 
    (∀t:struct_one. P (base t)) →  
    (∀O. P (lista O [ ])) → 
    (∀O.∀H.∀TL. P H → P ( lista O TL) → P (lista O (H::TL)) )→ 
    (∀S. P S)  .
    
  #P #HB #HN #HL #s
  cut (∃n. size_struct s =n)
  [% {(size_struct s)} //] (*La dimensione esiste sempre*)
  * #n lapply s -s @(nat_elim1 n) (*Induzione sulla dimensione*)
  -n #m #H #s cases s
  [ #T // (*Caso base*) 
  | (* Se s è una struttura con lista *)
    #O #l 
     cases l (*Induzione sulla lista interna *)
      [ (*Lista vuota*)
        #H1 // 
       | (*Lista con almeno un elemento *)
         #st #l1
          #H1
          @HL 
           [ (*Head*)
              @(H … (refl  …)) (*La dimenione della head è minore del totale?*)
              <H1 >(plus_n_O (size_struct st)) in ⊢ (?%?); whd
              >(plus_n_Sm (size_struct st) 0) in ⊢ (?%?); @monotonic_le_plus_r
              elim l1 (*Induzione sulla coda*) // #a #tl normalize /2/ 
           | (*Tail*)
              normalize in H1; lapply(sym_eq nat …H1)  >commutative_plus -H1 #H1 lapply (eq_plus_to_le … H1)-H1 
              elim l1 (*Induzione sulla coda*)
              // (*Coda vuota*)
              #b2 #l2 #Hind normalize #H1 @HL
              [ (*Spezzo la lista, Head*)
                @(H … (refl …)) @(lt_to_le_to_lt … H1) >(plus_n_O (size_struct b2)) in ⊢ (?%?); whd
               >(plus_n_Sm (size_struct b2) 0) in ⊢ (?%?); @monotonic_le_plus_r
               elim l2 // #a #tl normalize /2/
               |
              @Hind /2/
             ]] ]] qed.
             
              
lemma negbase : ∀t:struct_one.neg (neg (base t) )= (base t).
  #T elim T
   [ #I elim I #B #X elim B normalize // | // qed.
   
lemma neglista : ∀O.∀H.∀TL. 
  ((neg (neg H))=H) → 
  (neg (neg (lista O TL))=lista O TL) → 
  (neg (neg (lista O (H::TL))) = lista O (H::TL)).
  #O #H #TL
  #H1
  normalize #H2 @eq_f2 lapply H2 -H2 elim O // normalize
  #H2
  @eq_f2 //
  destruct // qed.

  
theorem negIdem : ∀s. neg (neg s) = s.
  @elim_struct
  [ @negbase | #O cases O normalize // | @neglista] qed.
  



  


                                                  (*                *
                                                   *   Uguaglianza  *
                                                   *    Riduzioni   *
                                                   *                *)
                                                   
inductive struct_eq : 𝐒→ 𝐒 → Prop ≝ 
 | eqComm : ∀S1,S2: 𝐒 .              S1 ≡ S2 → S2 ≡ S1
 | eqRif : ∀S1: 𝐒 .                  S1 ≡ S1
 | eqTrans : ∀S1,S2,S3: 𝐒 .          S1 ≡ S2 → S2 ≡ S3 → S1 ≡ S3
 
 | eqUnit : ∀S1,S2:𝐒.               filter_unit S1 ≡ filter_unit S2 → S1 ≡ S2
 
 
 | eqParComm : ∀L1.∀N1,N2.         lista par (L1) ≡ lista par (list_swap ? L1 N1 N2 (base unit))
 | eqCoparComm : ∀L1.∀N1,N2.       lista copar (L1) ≡ lista copar (list_swap ? L1 N1 N2 (base unit))

 | eqSingleton : ∀S1,S2.               singleton S1 ≡ singleton S2 → S1 ≡ S2 
 
 | eqAss : ∀L1,L2,L3,L4.∀O.             L1@L2@L3=L4 → lista O L4 ≡ lista O (L1@((lista O L2)::L3)) 
 
 | eqContext : ∀H1,H2.∀L1,L2.∀O.   H1 ≡ H2 → lista O L1 ≡ lista O L2 → lista O (H1::L1) ≡ lista O (H2::L2).
 

lemma eqAss2 :  ∀L1,L2,L3.∀O.           L1@L2=L3 → lista O L3 ≡ lista O ((lista O L1)::L2). 
  #L1 #L2 #L3 @(eqAss (nil ?) L1 L2 L3 ) qed.

inductive struct_reduce : 𝐒 → 𝐒→ Prop ≝ 
| reduceEq : ∀S1,S2:𝐒.    S1 ≡ S2 → S1 ⥤ S2
| reduceRif: ∀S.          S ⥤ S
| reduceTrans:  ∀S1,S2,S3: 𝐒 .          S1 ⥤ S2 → S2 ⥤ S3 → S1 ⥤ S3
| reduceA :  ∀n:nat.     (base unit) ⥤ 〚n+;n^〛
| reduceS : ∀R,T,U.      ❨ 〚R;T〛;U❩ ⥤ 〚❨R;U❩;T〛
| reduceQ : ∀R,T,U,V.     ❮〚R;U〛;〚T;V〛❯ ⥤ 〚❮R;T❯;❮U;V❯〛
| reduceContext : ∀H1,H2:𝐒.∀L1,L2.∀O. 
                H1 ⥤ H2 → (lista O L1) ⥤ (lista O L2) → (lista O (H1::L1)) ⥤  (lista O (H2::L2))
                
| reduceNeg : ∀S,T. neg S ⥤ neg T → S⥤T (*QUESTA PROBABILMENte SI PUÒ DERIVARE, MA NON RIESCO*).

lemma par_swap : ∀S1,S2. 〚S1;S2〛≡ 〚S2;S1〛.
#S1 #S2 
@(eqTrans ? (lista par (list_swap ? [S1;S2] 0 1 (base unit))) ?) // qed.

lemma copar_swap : ∀S1,S2. ❨S1;S2❩≡ ❨S2;S1❩.
#S1 #S2 
@(eqTrans ? (lista copar (list_swap ? [S1;S2] 0 1 (base unit))) ?) // qed.


lemma unit_to_some_par_base : ∀t. ∘ ⥤ 〚base t;neg(base t)〛.
  #t 
  elim t
  [ #I elim I #B #N elim B // normalize 
  @reduceTrans
  [ @〚N+;N^〛 ] // @reduceEq 
  @eqTrans
  [ @(lista par (list_swap ? [N+;N^] 0 1 (base unit))) ]
  //]
  normalize 
  @reduceEq @eqComm 
  @eqTrans [ @〚∘〛 | @eqUnit normalize // | @eqSingleton normalize //] qed.
  
lemma lista_nil_to_unit : ∀o. lista o [ ] ≡ ∘.
  #O
  @(eqTrans ? (lista O [∘]) ?) 
  [@eqUnit normalize // | @eqSingleton normalize //]
  qed.
  
lemma unit_to_s_ns_nil : ∀o. ∘ ⥤ 〚lista o [ ] ; neg (lista o [ ])〛.
  #O @reduceEq
  @eqComm 
  @(eqTrans ? 〚(lista O [ ])〛 ?)
  [ @eqContext // elim O normalize @eqSingleton normalize] /2/
  @(eqTrans ? ∘ ? ) //
  @eqComm // qed.
  
lemma unit_to_s_ns_list :   ∀O.∀H.∀TL.
  ∘⥤ 〚H;neg H〛 → 
  ∘⥤ 〚lista O TL;neg (lista O TL) 〛 → 
  ∘⥤〚lista O (H::TL); neg (lista O (H::TL))〛.
  #O #H #TL #H1
  cases O  #H2 normalize (*Per casi sugli operatori*)
        [
        @(reduceTrans ? 〚(lista copar (neg H::map ? ? neg TL)); (lista par (H::TL))〛?)
        [ | @reduceEq @par_swap]]
        [1,2:
        [letin head ≝H letin tail ≝ TL letin nHead ≝ (neg H) letin nTail ≝ (map ? ? neg TL)
        | letin head ≝ (neg H) letin tail ≝(map ? ? neg TL) letin nHead ≝ H letin nTail ≝ TL ]
        

        (*Ora devo creare U grazie l'associatività*)

        @(reduceTrans ? (〚(❨nHead;(lista copar (nTail))❩); (lista par (head::tail))〛) ?)

           [2,4: @reduceEq @eqComm @eqContext [1,3:  @eqContext // @eqAss2 //] //]

        (*Ora posso applicare la riduzione sulla parte destra*)

        @(reduceTrans ? (❨〚nHead; (lista par (head::tail))〛; (lista copar nTail)❩) ?)
           [2,4: @reduceS]

        (*Ora devo accoppiare H e neg H*)

        @(reduceTrans ? (❨〚(nHead); head;(lista par (tail))〛; (lista copar nTail)❩) ?)
          [2,4: @reduceEq @eqContext // 
          
          @eqContext //
          
            @(eqTrans ? ((lista par (head::tail))) ?)
              [1,3: @eqComm @(eqAss [head] ? ? ?) normalize // |2,4: @eqSingleton normalize //]]
              
        @(reduceTrans ? ❨〚〚nHead; head〛; (lista par tail)〛; (lista copar nTail)❩)
          [2,4:  @reduceEq @eqComm 
            @eqContext // @(eqAss (nil ?) ([nHead;head]) ) //]
        @(reduceTrans ? (❨〚∘; (lista par tail)〛; (lista copar nTail)❩))
        [2,4: @reduceContext // @reduceContext // 
          @(reduceTrans ?(〚head;nHead〛)?) [2,4: @reduceEq//] @H1]
          @reduceNeg normalize
          lapply (negIdem (lista par TL)) #nTL normalize in nTL; >nTL -nTL
(*          lapply (negIdem (lista copar TL)) #nTL normalize in nTL; >nTL -nTL*)
          @(reduceTrans ? 〚❨(lista copar (map ? ? neg tail))❩; (lista par tail)〛 ? )
          [2,4: @reduceEq @eqUnit //] 
          @(reduceTrans ? 〚(lista copar (map ? ? neg tail)); (lista par tail)〛 ? )
          [2,4: @reduceEq @eqSingleton //]
          @(reduceTrans ? 〚(lista par tail);(lista copar (map ? ? neg tail))〛 ? )
          [2,4: @reduceEq @par_swap] 
          normalize in H2; [ @H2 | normalize
          lapply (negIdem (lista copar TL)) #nTL normalize in nTL; >nTL -nTL
          @(reduceTrans ? 〚(lista copar TL); (lista par (map ? ? neg TL))〛 ? )
          [ | @reduceEq @par_swap] @H2   ]
          |
     
       (*  Voglio poter applicare questa   ❮〚R;U〛;〚T;V〛❯ ⥤ 〚❮R;T❯;❮U;V❯〛*)
          (* Porto il copar sulla sinistra*)

        (*Ora devo creare R grazie l'associatività*)
        letin nHead ≝H letin nTail ≝ TL letin head ≝ (neg H) letin tail ≝ (map ? ? neg TL) 
        @(reduceTrans ? (〚(❮nHead;(lista seq (nTail))❯); (lista seq (head::tail))〛) ?)

           [| @reduceEq @eqComm @eqContext [ @eqContext // @eqAss2 //] //]

        (*Ora devo creare U*)
        
        @(reduceTrans ? (〚❮nHead; (lista seq nTail)❯; ❮head;(lista seq (tail))❯〛) ?)
         [| @reduceEq @eqComm @eqContext [ @eqContext //] @eqContext // @(eqAss ([head]) ? ? ?) normalize //]
         
        
        (*Ora posso applicare la riduzione sulla parte destra*)
        @(reduceTrans ? (❮〚nHead;head〛;〚(lista seq nTail);(lista seq tail)〛❯) ?)

           [ |@reduceQ]

        @(reduceTrans ? (❮∘; 〚(lista seq nTail); (lista seq tail) 〛❯))
        
        [ | @reduceContext //]
        normalize
        @(reduceTrans ? (❮∘;∘❯))
        [2: @reduceContext // @reduceContext] //
        @reduceEq @eqUnit normalize @eqComm // qed.


theorem unit_to_s_ns : ∀s. ∘⥤ 〚s;neg s〛.
  @elim_struct /2/ qed.
                                                   

